Lean 4 on GitHub Actions
キャッシュについて
Lean 4で書かれた証明/コードをGitHub Actionsでビルドするとき何をキャッシュすれば良いのか調べたが，よくわからなかった．
elanを導入すればLakeが勝手に入ってくるのでlake buildとすればいい．
問題はlake buildはMathlib4とかに依存しているとバカみたいに長いということがあり…
素朴に考えれば/lake-packagesと/buildをキャッシュすればいい
が，依存先が/buildに生成物を吐き出すかどうかはlakefile.leanで変更できるようだ
https://github.com/leanprover/lake#layout buildDirの部分
すなわち/lake-packages/{packageName}/buildかどうかは実際にはよくわからない
別にそうでないものを無視して，決め打ちでいいならもうこの話はここで終わりである
そもそもこれを本当にキャッシュして良いものなのかはわからない．
lean-toolchainとlake-manifest.jsonをキーにしてキャッシュすれば問題はないと思う
検証していないので（面倒だった）
LakeのIssue見てみたがそもそもキャッシュしたいという欲求がそんなに無いのか？
GitHub ActionsでそもそもLeanのコードをビルドしている例が少ない．
そもそもLeanのリポジトリが少ない．
まあLeanでコード書くときに頻繁にプッシュしないからCIに5分かかっても良いか！となって調査を終了してしまった
そもそもこれはMathlibに依存している場合のみであり，他のケースでビルド時間がどのぐらいになりそうなのか検討もつかない．